\documentclass[12pt]{article}
\usepackage{fullpage,cmu-titlepage2}
\usepackage{times}
\usepackage{excludeonly}
%\usepackage{semantic}

\usepackage[T1]{fontenc}

% 
% THIS TEST BELOW DOES NOT SEEM TO WORK CORRECTLY. I COMMENTED
% IT OUT SINCE WE ARE NOT USING GRAPHICS, BUT LET ME KNOW IF
% YOU NEED GRAPHICS AND WE CAN FIGURE OUT A SOLUTION.
%
%Check if we are compiling under latex or pdflatex
%\ifx\pdftexversion\undefined
%  \usepackage[dvips]{graphics}
%\else
%  \usepackage[pdftex]{graphics}
%\fi

%\usepackage{longtable,listings,tabulary,MnSymbol,float,graphicx, mathpartir}
\usepackage{amssymb}
\usepackage{listings}
\usepackage{mathpartir}
\usepackage{graphicx}

%\usepackage{amsthm}
%\usepackage{amssymb}
%\usepackage{amsmath}
%\usepackage{rotating}
\usepackage{tabularx}
\usepackage[
%backref controls whether the bibliography has a list of backreferences
%to where the citaiton is used
%backref,
pageanchor=true,
plainpages=false,
pdfpagelabels, % makes the status line page labels the same as latex ones
bookmarks,
bookmarksnumbered,
pdfborder=0 0 0,
pdfpagemode=UseOutlines]{hyperref}
%\usepackage{draftstamp}
%\usepackage{subfigure}

%\include{defns}

\usepackage[release]{PlaidDefinitions}

\newcommand{\singlespace}{\renewcommand{\baselinestretch}{1.0}\normalsize}

\newcommand{\vI}[1]{#1}
\newcommand{\vII}[1]{}

\excludeonly{types}



% Provides a draft mark at the top of the document. Comment this out
% to remove it
%\draftstamp{\today}{DRAFT}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\title{The Plaid Language:\\
Dynamic Core Specification\\ %and Rationale\\
\vspace{2ex}
version 0.1.2\\
\vspace{2ex}
}

\author{Jonathan Aldrich$^{\ast}$
}
% TODO: credit to those who made substantial contributions to the definitions
% or text
% Nels - overall document structure & standards
% Eric - PLT Scheme core
% Darpan - formal semantics for core


\date{June 2010}

\abstract{
Plaid is the first typestate-oriented programming language.
Typestate-oriented programming extends the object-oriented
programming paradigm so that each object has a state that
can change as a program executes.  Each state has its own
interface, behavior, and representation.  Plaid combines
a pure object model with good support for functional
programming.
\\
\\
\indent
This document defines the syntax and semantics of the
dynamically-typed core of the Plaid language.
}





\keywords{programming language, specification, typestate, Plaid}

\trnumber{}

\citationinfo{
%$^{\dag}$Harry doesn't actually exist, so he has no address. \\
$^{\ast}$School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, USA \\
}

%\arpasupport{fox}
\support{This research is supported by DARPA grant HR00110710019 and
NSF grant CCF-0811592.}
% \authorsupport{The author holds a Froboz Gradual Fellowship.}

% \otherdisclaimer{NSF}

\begin{document}
\renewcommand*{\thepage}{title-\arabic{page}} 
\maketitle
\renewcommand*{\thepage}{\arabic{page}} 





%%%%%%%%%%%%%%%%%%%% MAIN TEXT %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\input{spec-shared}

\end{document}
